{-# LANGUAGE FlexibleContexts, FlexibleInstances,
  ScopedTypeVariables, OverloadedStrings, TupleSections, ViewPatterns #-}
module Core.Lint
  ( CoreError
  , runLint, runLintOK, emptyScope
  , checkStmt, checkTerm, checkAtom, checkType
  ) where

import Control.Applicative.Lift
import Control.Monad.Writer
import Control.Monad.Except
import Control.Applicative
import Control.Lens

import qualified Data.VarMap as VarMap
import qualified Data.VarSet as VarSet
import qualified Data.Sequence as Seq
import qualified Data.Text as T
import Data.Functor.Constant
import Data.Traversable
import Data.Bifunctor
import Data.Foldable
import Data.Function
import Data.Functor
import Data.Text ()
import Data.Maybe
import Data.Tuple
import Data.List

import Core.Optimise
import Core.Builtin
import Core.Types

import Text.Pretty.Semantic hiding ((<>))
import Text.Pretty.Annotation

data CoreError
  = TypeMismatch Type Type
  | InfoMismatch CoVar VarInfo VarInfo
  | InfoIllegal CoVar VarInfo VarInfo
  | NoSuchVar CoVar
  | IllegalUnbox
  | InvalidCoercion Coercion
  | PatternMismatch [(CoVar, Type)] [(CoVar, Type)]

type CoreErrors = (Seq.Seq CoreError)

type LintResult = Sum Int

data Scope = Scope { vars :: VarMap.Map (Type, VarInfo)
                   , types :: VarMap.Map VarInfo
                   , tyVars :: VarSet.Set }
  deriving (Show)

emptyScope :: Scope
emptyScope = Scope (VarMap.fromList (map (\(a, b) -> (a, (b, varInfo a))) builtinVarList))
                   (VarMap.fromList (map (,TypeConVar) builtinTyList))
                   mempty

insertVar :: IsVar a => a -> Type -> VarMap.Map (Type, VarInfo) -> VarMap.Map (Type, VarInfo)
insertVar v t = VarMap.insert (toVar v) (t, varInfo v)

insertTy :: IsVar a => a -> VarMap.Map VarInfo -> VarMap.Map VarInfo
insertTy v = VarMap.insert (toVar v) (varInfo v)

instance Pretty CoreError where
  pretty (TypeMismatch l r) = text "Expected type" <+> pretty l </>
                              text "     got type" <+> pretty r
  pretty (InfoMismatch v l r) = text "Expected var info" <+> string (show l) </>
                                text "     got var info" <+> string (show r) </>
                                text "for" <+> pretty v
  pretty (InfoIllegal v l r) = text "Expected var info like" <+> string (show l) </>
                               text "          got var info" <+> string (show r) </>
                               text "for" <+> pretty v
  pretty (NoSuchVar a) = text "No such variable" <+> pretty a
  pretty IllegalUnbox = text "Illegal unboxed type"
  pretty (InvalidCoercion a) = text "Illegal coercion" <+> pretty a
  pretty (PatternMismatch l r) = text "Expected vars" <+> pVs l </>
                                 text "     got vars" <+> pVs r
    where pVs = hsep . punctuate comma . map (\(v, ty) -> pretty v <+> colon <+> pretty ty)
          pVs :: [(CoVar, Type)] -> Doc

  prettyList = vsep . map pretty

instance Annotation CoreError where
  annotated e a = serror ("(* XXX" <+> align (pretty e) <+> "*)") <#> a

instance Annotation (Seq.Seq CoreError) where
  annotated = flip (foldr annotated)

instance Pretty a => Pretty [(AnnStmt CoreErrors a, CoreErrors)] where
  pretty = vsep . map (\(s, es) -> annotated es (pretty s))

runLint :: Pretty b
        => String -> Writer LintResult b
        -> c -> c
runLint context m res =
  case runLintOK m of
    Nothing -> res
    Just (c, e) -> error . T.unpack . displayDetailed $
     string ("Core lint failed after `" ++ context ++ "` with " ++ show c ++ " errors") <#>
     pretty e

runLintOK :: Writer LintResult b -> Maybe (Int, b)
runLintOK m = case runWriter m of
                (_, Sum 0) -> Nothing
                (x, Sum c) -> Just (c, x)

checkStmt :: (IsVar a, MonadWriter LintResult m)
          => Scope
          -> [Stmt a]
          -> m [(AnnStmt CoreErrors a, CoreErrors)]
checkStmt _ [] = pure []
checkStmt s (Foreign v ty b:xs) = do
  es <- gatherError' . liftError $
    -- Ensure we're declaring a value
       unless (varInfo v == ValueVar) (pushError (InfoIllegal (toVar v) ValueVar (varInfo v)))
    -- And the type is well formed
    *> checkType s ty

  ((Foreign v ty b, es):) <$> checkStmt (s { vars = insertVar v ty (vars s) }) xs

checkStmt s (StmtLet (One (v, ty, e)):xs) = do
  (ty', e') <- checkTerm s e

  es <- gatherError' . liftError $
    -- Ensure type is valid and we're declaring a value
    (case ty' of
       Just ty' | ty `apart` ty' -> pushError (TypeMismatch ty ty')
       _ -> pure ())
    *> unless (varInfo v == ValueVar) (pushError (InfoIllegal (toVar v) ValueVar (varInfo v)))
    *> checkType s ty

  ((StmtLet (One (v, ty, e')), es):) <$> checkStmt (s { vars = insertVar v ty (vars s) }) xs
checkStmt s (StmtLet (Many vs):xs) = do
  let s' = s { vars = foldr (\(v, t, _) -> insertVar v t) (vars s) vs }

  (vs', es) <- forMA vs $ \(v, ty, e) -> do
    (ty', e') <- checkTerm s' e
    es <- gatherError' . liftError $
      -- Ensure type is valid and we're declaring a value
      (case ty' of
         Just ty' | ty `apart` ty' -> pushError (TypeMismatch ty ty')
         _ -> pure ())
      *> unless (varInfo v == ValueVar) (pushError (InfoIllegal (toVar v) ValueVar (varInfo v)))
      *> checkType s ty
    pure ((v, ty, e'), es)

  ((StmtLet (Many vs'), es):) <$> checkStmt s' xs

checkStmt s (Type v ctors:xs) = do
  let s' = s { vars = foldr (uncurry insertVar) (vars s) ctors
             , types = foldr insertTy (types s) (toVar v : map (toVar . fst) ctors)}

  es <- gatherError' . liftError $
    -- Ensure we're declaring a type
       unless (varInfo v == TypeConVar) (pushError (InfoIllegal (toVar v) TypeConVar (varInfo v)))
    *> for_ ctors (\(v, x) ->
         -- Ensure we're declaring a constructor
         unless (varInfo v == DataConVar) (pushError (InfoIllegal (toVar v) DataConVar (varInfo v)))
          -- Ensure the type is well formed
         *> checkType s' x)

  ((Type v ctors, es):) <$> checkStmt s' xs

checkAtom :: Scope -> Atom -> Errors CoreErrors Type
checkAtom s (Ref v ty) =
  case VarMap.lookup (toVar v) (vars s) of
    Nothing -> pushError (NoSuchVar v)
    Just (ty', inf')
      -- Ensure the types line up
      | ty `apart` ty' -> pushError (TypeMismatch ty' ty)
      -- Ensure the variable info lines up, and it's a valid variable
      | inf' /= varInfo v -> pushError (InfoMismatch v inf'(varInfo v))
      | not (isValueInfo inf') -> pushError (InfoIllegal v ValueVar inf')
      | otherwise -> pure ty
checkAtom _ (Lit l) = pure (litTy l)

checkTerm :: forall a m. (IsVar a, MonadWriter LintResult m)
         => Scope
         -> Term a
         -> m (Maybe Type, AnnTerm CoreErrors a)
checkTerm s (Atom a) = do
  res <- gatherError (liftError (checkAtom s a))
  pure (flip AnnAtom a <$> res)

checkTerm s (App f x) = do
  res <- gatherError $ do
    (f', x') <- liftError $ (,) <$> checkAtom s f <*> checkAtom s x
    case f' of
      ForallTy Irrelevant a r | a `uni` x' -> pure r
      _ -> chuckError (TypeMismatch (ForallTy Irrelevant x' unknownTyvar) f')
  pure ((\es -> AnnApp es f x) <$> res)

checkTerm s (Lam arg@(TermArgument a ty) bod) = do
  errs <- gatherError' . liftError $
    -- Ensure type is valid and we're declaring a value
       unless (varInfo a == ValueVar) (pushError (InfoIllegal (toVar a) ValueVar (varInfo a)))
    *> checkType s ty

  (bty, bod') <- checkTerm (s { vars = insertVar a ty (vars s) }) bod
  pure ( ForallTy Irrelevant ty <$> bty
       , AnnLam errs arg bod')
checkTerm s (Lam arg@(TypeArgument a ty) bod) = do
  errs <- gatherError' . liftError $
    -- Ensure type is valid and we're declaring a tyvar
       unless (varInfo a == TypeVar) (pushError (InfoIllegal (toVar a) TypeVar (varInfo a)))
    *> checkType (s { tyVars = VarSet.insert (toVar a) (tyVars s) }) ty

  (bty, bod') <- checkTerm (s { tyVars = VarSet.insert (toVar a) (tyVars s) }) bod
  pure ( ForallTy (Relevant (toVar a)) ty <$> bty
       , AnnLam errs arg bod')

checkTerm s (Let (One (v, ty, e)) r) = do
  (ty', e') <- checkTerm s e
  (tyr, r') <- checkTerm (s { vars = insertVar v ty (vars s) }) r

  es <- gatherError' . liftError $
    -- Ensure type is valid and we're declaring a value
    (case ty' of
       Just ty' | ty `apart` ty' -> pushError (TypeMismatch ty ty')
       _ -> pure ())
    *> unless (varInfo v == ValueVar) (pushError (InfoIllegal (toVar v) ValueVar (varInfo v)))
    *> checkType s ty

  pure ( tyr, AnnLet es (One (v, ty, e')) r')

checkTerm s (Let (Many vs) r) = do
  let s' = s { vars = foldr (\(v, t, _) -> insertVar v t) (vars s) vs }

  (vs', es) <- forMA vs $ \(v, ty, e) -> do
    (ty', e') <- checkTerm s' e
    es <- gatherError' . liftError $
      -- Ensure type is valid and we're declaring a value
      (case ty' of
         Just ty' | ty `apart` ty' -> pushError (TypeMismatch ty ty')
         _ -> pure ())
      *> unless (varInfo v == ValueVar) (pushError (InfoIllegal (toVar v) ValueVar (varInfo v)))
      *> checkType s ty
    pure ((v, ty, e'), es)

  (tyr, r') <- checkTerm s' r
  pure ( tyr, AnnLet es (Many vs') r')

checkTerm s (Match e bs) = do
  (tye, es) <- gatherError . liftError $ checkAtom s e

  -- Build up our arms and verify they are well formed
  (unzip -> (tys, bs'), es') <- forMA bs $
    \Arm { _armPtrn = p, _armTy = ty, _armBody = r, _armVars = vs, _armTyvars = tvs } -> do
      let pVars = patternVars p
      (tyr, r') <- checkTerm (s { vars = foldr (uncurry insertVar) (vars s) pVars
                                , tyVars = tyVars s <> foldMap (freeInTy . snd) pVars }) r
      es <- gatherError' . liftError $
        (case tye of
           Just tye | ty `apart` tye -> pushError (TypeMismatch ty tye)
           _ -> pure ())
        *> when (vs /= patternVars p) (pushError (PatternMismatch (first toVar <$> patternVars p) (first toVar <$> vs)))
        *> checkPattern s ty p
      pure ((tyr, Arm p ty r' vs tvs), es)

  -- Verify the types are consistent
  let ty = foldr1 (<|>) tys
  es'' <- gatherError' . liftError . for_ tys $ \ty' ->
    case (ty, ty') of
      (Just ty, Just ty') | ty `apart` ty' -> pushError (TypeMismatch ty ty')
      _ -> pure ()

  pure ( ty, AnnMatch (es <> es' <> es'') e bs')

checkTerm s (Extend f fs) = do
  res <- gatherError $ do
    tyf' <- liftError $
         for_ fs (\(_, ty, v) ->
           (\ty' -> if ty `apart` ty' then pushError (TypeMismatch ty ty') else pure ())
           <$> checkAtom s v)
      *> checkAtom s f

    pure $ case tyf' of
      RowsTy tau rs ->
        let updated = deleteFirstsBy ((==) `on` fst) rs tys
            tys = map (\(f, ty, _) -> (f, ty)) fs
            inner = case updated of
              [] -> tau
              xs -> RowsTy tau xs
         in RowsTy inner tys
      x -> RowsTy x . map (\(f, ty, _) -> (f, ty)) $ fs

  pure ((\es -> AnnExtend es f fs) <$> res)

checkTerm s (Values xs) = do
  (ty, es) <- gatherError . liftError $ for xs (checkAtom s)
  pure (ValuesTy <$> ty, AnnValues es xs)

checkTerm s (TyApp f x) = do
  res <- gatherError $ do
    (f', ()) <- liftError $ (,) <$> checkAtom s f <*> checkTypeBoxed s x
    case f' of
      ForallTy (Relevant a) _ ty -> pure (substituteInType (VarMap.singleton (toVar a) x) ty)
      _ -> chuckError (TypeMismatch (ForallTy (Relevant unknownVar) unknownTyvar unknownTyvar) f')

  pure ((\es -> AnnTyApp es f x) <$> res)

checkTerm s (Cast x expTo co) = do
  res <- gatherError $ do
    (ty, (from, to)) <- liftError $ (,) <$> checkAtom s x <*> checkCoercion s co
    when (from `apart` ty) (chuckError (TypeMismatch from ty))
    when (to `apart` expTo) (chuckError (TypeMismatch expTo to))
    pure to

  pure ((\es -> AnnCast es x expTo co) <$> res)

-- | Verify a type is valid within the given scope
--
-- TODO: We should really verify the kinds match up, but we're a long way away
-- from that working
checkType :: Scope -> Type -> Errors CoreErrors ()
checkType s (ConTy v) =
  case VarMap.lookup v (types s) of
    Nothing -> pushError (NoSuchVar v)
    Just inf | not (isTypeInfo inf) -> pushError (InfoIllegal v TypeConVar inf)
             | otherwise -> pure ()
checkType _ (VarTy v)
  | varInfo v /= TypeVar = pushError (InfoIllegal v TypeVar (varInfo v))
  | otherwise = pure ()
checkType s (ForallTy Irrelevant a r) = checkType s a *> checkTypeBoxed s r
checkType s (ForallTy (Relevant vs) c v) =
  let s' = s { tyVars = VarSet.insert (toVar vs) (tyVars s) }
  in unless (varInfo vs == TypeVar) (pushError (InfoIllegal vs TypeVar (varInfo vs)))
  *> checkType s' c
  *> checkType s' v
checkType s (AppTy f x) = checkType s f *> checkTypeBoxed s x
checkType s (RowsTy f fs) = checkType s f *> traverse_ (checkTypeBoxed s . snd) fs
checkType s (ValuesTy xs) = traverse_ (checkTypeBoxed s) xs
checkType _ StarTy = pure ()
checkType _ NilTy = pure ()

checkTypeBoxed :: Scope -> Type -> Errors CoreErrors ()
checkTypeBoxed s x = checkType s x *> checkNoUnboxed x

-- | Check a coercion is well formed within a given scope, returning the input
-- and output types.
--
-- Ideally this would use ApplicativeDo, but GHC is still a little silly at
-- desugaring it all.
checkCoercion :: Scope -> Coercion -> Errors CoreErrors (Type, Type)
checkCoercion s = checkCo where
  checkCo :: Coercion -> Errors CoreErrors (Type, Type)
  checkCo (SameRepr a b) =
       checkType s a
    *> checkType s b
    $> (a, b)
  checkCo (Application l r) =
    (\(f, g) (x, y) -> (AppTy f x, AppTy g y))
    <$> checkCo l
    <*> checkCo r
  checkCo (ExactRecord rs) =
    bimap ExactRowsTy ExactRowsTy . unzip
    <$> for rs (\(t, c) -> (\(a, b) -> ((t, a), (t, b))) <$> checkCo c)
  checkCo (Record c rs) =
    (\(a, b) (as, bs) -> (RowsTy a as, RowsTy b bs))
    <$> checkCo c
    <*> fmap unzip (for rs (\(t, c) -> (\(a, b) -> ((t, a), (t, b))) <$> checkCo c))
  checkCo (Projection rs rs') =
    (\(as, bs) (ss, ts) ->
       let first = unionBy ((==) `on` fst) as ss
       in (ExactRowsTy first, RowsTy (ExactRowsTy bs) ts))
    <$> fmap unzip (for rs (\(t, c) -> (\(a, b) -> ((t, a), (t, b))) <$> checkCo c))
    <*> fmap unzip (for rs' (\(t, c) -> (\(a, b) -> ((t, a), (t, b))) <$> checkCo c))

  checkCo (CoercionVar x) =
    case VarMap.lookup (toVar x) (vars s) of
      Just (AppTy (AppTy _ l) r, _) -> pure (l, r)
      Just _ -> pushError (InvalidCoercion (CoercionVar x))
      _ -> pure (VarTy (fromVar tyvarA), VarTy (fromVar tyvarB))

  checkCo (Nth co i) =
    case VarMap.lookup (toVar co) (vars s) of
      Just (ExactRowsTy rs, _) | (_, AppTy (AppTy _ l) r) <- rs !! i -> pure (l, r)
      _ -> pushError (InvalidCoercion (Nth co i))

  checkCo (Axiom ax i) =
    case VarMap.lookup (toVar ax) (vars s) of
      Just (pi, _) -> checkCoAx (Axiom ax i) pi i
      _ -> pushError (InvalidCoercion (Axiom ax i))

  checkCo (Symmetry x) = swap <$> checkCo x
  checkCo co@(Trans x y) =
    (\((tx, ty), (ty', tz)) ->
       (if ty `apart` ty'
        then failure (Seq.fromList [ InvalidCoercion co, TypeMismatch ty ty' ])
        else pure ())
       $> (tx, tz)) `bindErrors` ((,) <$> checkCo x <*> checkCo y)
  checkCo (Quantified v l r) =
    (\(f, g) (x, y) -> (ForallTy v f x, ForallTy v g y)) <$> checkCo l <*> checkCo r

  coAxT (ForallTy Irrelevant (AppTy (AppTy _ l) r) rest) = (l, r):coAxT rest
  coAxT (ForallTy Relevant{} _ rest) = coAxT rest
  coAxT (AppTy (AppTy _ l) r) = [(l, r)]
  coAxT x = error (show x)

  checkCoAx _ (coAxT -> ts) args =
    (\sub -> bimap (substituteInType sub) (substituteInType sub) (last ts)) . fold
      <$> traverse checkCo' (zip ts args)

  checkCo' ((a, b), co) =
    (\(l, r) ->
      case (unify a l, unify b r) of
         (Just a, Just b) -> pure ((a <> b) `VarMap.withoutKeys` VarSet.toList (tyVars s))
         (_, _) -> pushError (InvalidCoercion co))
    `bindErrors` checkCo co

checkPattern :: forall a. IsVar a => Scope -> Type -> Pattern a -> Errors CoreErrors ()
checkPattern s = checkPat where
  checkCapture :: Type -> Capture a -> Errors CoreErrors ()
  checkCapture ty' (Capture a ty)
    | ty `apartOpen` ty' = pushError (TypeMismatch ty ty')
    | varInfo a /= ValueVar = pushError (InfoIllegal (toVar a) ValueVar (varInfo a))
    | otherwise = pure ()

  checkPat :: Type -> Pattern a -> Errors CoreErrors ()
  checkPat _ PatWildcard = pure mempty
  checkPat (RowsTy _ _) (PatLit RecNil) = pure mempty
  checkPat NilTy (PatLit RecNil) = pure mempty
  checkPat ty' (PatLit l) =
    let ty = litTy l
    in when (ty `apart` ty') (pushError (TypeMismatch ty ty'))
    $> mempty
  checkPat ty' (Constr a) =
    case VarMap.lookup (toVar a) (vars s) of
      Nothing -> pushError (NoSuchVar (toVar a))
      Just (ty, inf)
        -- Ensure types line up
        | inst ty `apartOpen` ty' -> pushError (TypeMismatch ty' (inst ty))
        -- Ensure we're matching on a constructor
        | inf /= varInfo a -> pushError (InfoMismatch (toVar a) inf (varInfo a))
        | inf /= DataConVar  -> pushError (InfoMismatch (toVar a) DataConVar (varInfo a))
        | otherwise -> pure mempty
  checkPat ty' (Destr a p) =
    case VarMap.lookup (toVar a) (vars s) of
      Nothing -> pushError (NoSuchVar (toVar a))
      Just (ty, inf)
        -- Ensure we're matching on a constructor
        | inf /= varInfo a -> pushError (InfoMismatch (toVar a) inf (varInfo a))
        | inf /= DataConVar  -> pushError (InfoMismatch (toVar a) DataConVar (varInfo a))
        -- Ensure types line up
        | (qs, r) <- splitForallTy $ inst ty
        , Just s <- r `unify` ty'
        -> () <$ zipWithM checkCapture (map (substituteInType s) qs) p
        | otherwise -> pushError (TypeMismatch (ForallTy Irrelevant unknownTyvar ty') (inst ty))
  checkPat (RowsTy _ _) (PatRecord []) = pure mempty
  checkPat NilTy (PatRecord []) = pure mempty
  checkPat ty@(RowsTy NilTy ts) (PatRecord fs) =
    let outer = filter (\(l, _) -> any ((== l) . fst) fs) ts
    in for_ fs (\(t, p) -> case find ((==t) . fst) outer of
         Nothing -> pushError (TypeMismatch (RowsTy NilTy [(t, unknownTyvar)]) ty)
         Just (_, ty) -> checkCapture ty p)
  checkPat ty@(RowsTy ext ts) (PatRecord fs) =
    for_ fs (\(t, p) -> case find ((==t) . fst) ts of
      Nothing -> pushError (TypeMismatch (RowsTy ext [(t, unknownTyvar)]) ty)
      Just (_, ty) -> checkCapture ty p)
  checkPat t (PatRecord fs) =
    pushError (TypeMismatch (RowsTy unknownTyvar (map (\(a, _) -> (a, unknownTyvar)) fs)) t)
  checkPat (ValuesTy ts) (PatValues ps) | length ts == length ps =
    traverse_ (uncurry checkCapture) (zip ts ps)
  checkPat t (PatValues ps) =
    pushError (TypeMismatch (ValuesTy (replicate (length ps) unknownTyvar)) t)

  inst (ForallTy (Relevant _) _ t) = inst t
  inst t = t
  splitForallTy (ForallTy Irrelevant q t) = splitForallTy t & _1 %~ (q:)
  splitForallTy t = ([], t)

checkNoUnboxed :: Type -> Errors CoreErrors ()
checkNoUnboxed ValuesTy{} = pushError IllegalUnbox
checkNoUnboxed _ = pure ()

unknownVar :: IsVar a => a
unknownVar = fromVar (CoVar (-100) (Just "?") ValueVar)

unknownTyvar :: Type
unknownTyvar = VarTy unknownVar

-- | Throw an error within an applicative
pushError :: CoreError -> Errors CoreErrors b
pushError = failure . pure

-- | Throw an error within an error monad
chuckError :: MonadError CoreErrors m => CoreError -> m b
chuckError = throwError . pure

-- | Lift an 'Errors' into an error monad
liftError :: MonadError CoreErrors m => Errors CoreErrors b -> m b
liftError m = case runErrors m of
                Left e -> throwError e
                Right x -> pure x

gatherError :: MonadWriter LintResult m => ExceptT CoreErrors m b -> m (Maybe b, CoreErrors)
gatherError m = do
  res <- runExceptT m
  case res of
    Left e -> tell (Sum (Seq.length e)) >> pure (Nothing, e)
    Right x -> pure (Just x, mempty)

gatherError' :: MonadWriter LintResult m => ExceptT CoreErrors m () -> m CoreErrors
gatherError' = fmap snd . gatherError

forMA :: (Monoid m, Applicative f) => [a] -> (a -> f (b, m)) -> f ([b], m)
forMA vs f = foldr (\x a ->
                      (\(a, b) (a', b') -> (a : a', b <> b'))
                      <$> f x <*> a) (pure mempty) vs

litTy :: Literal -> Type
litTy (Int _) = tyInt
litTy (Str _) = tyString
litTy (Float _) = tyFloat
litTy LitTrue = tyBool
litTy LitFalse = tyBool
litTy Unit = tyUnit
litTy RecNil = NilTy

uni, apart, uniOpen, apartOpen :: Type -> Type -> Bool
uni = uniOpen
apart a b = not (uni a b)
uniOpen a b = isJust (unify a b)
apartOpen a b = not (uniOpen a b)

patternVars :: Pattern a -> [(a, Type)]
patternVars (Destr _ p) = map captureVars p
patternVars (PatRecord ps) = map (captureVars . snd) ps
patternVars (PatValues ps) = map captureVars ps
patternVars Constr{} = []
patternVars PatLit{} = []
patternVars PatWildcard{} = []

captureVars :: Capture a -> (a, Type)
captureVars (Capture v ty) = (v, ty)

bindErrors :: (a -> Errors e b) -> Errors e a -> Errors e b
bindErrors f (Pure a) = f a
bindErrors _ (Other (Constant x)) = failure x
